#define USERS	2
/* Bidder1 States */

mtype = {idleB, startB, submittedB};

/* Auctioneer States */

mtype ={waitA, startA, processBidA, endA};

/* Events*/

mtype = {start_auction, auction_started, status, winner, loser, end_auction, dummy, send_bid};

mtype stateA;
bool givenUp;
bool gUp[USERS];

/* channels for transitions */	

int amountOfClients = USERS;
int startBid=13;
int nrounds = 3;

chan m2A = [0] of {int, int, mtype};
chan m2B[USERS] = [0] of {int, mtype};

/* Winning client */
int clientId;
int clientBid;

init {
    int i = 0;
    do
    :: (i<amountOfClients) -> run client(i); gUp[i] = false;
        i = i+1;
    :: (i==amountOfClients) -> break;
    od;
    run auctioneer();
    m2A!0, 0, start_auction;
    printf("Msg to start the auction\n");
}

/*Client process*/

proctype client(int id) {
    mtype stateB = idleB;
    do
    :: m2B[id]?0, auction_started ->
        printf("The auction is now open, the client %d knows",id);
    :: m2B[id]?0, end_auction -> printf("Auction is terminating \n");
        break;
    :: m2B[id]?0,send_bid -> printf("Ready to submit a bid\n");
        printf("Sending bid \n");
        atomic {
            if
            :: skip -> m2A!12, id, dummy;
            :: skip -> m2A!13, id, dummy;
            :: skip -> m2A!14, id, dummy;
            :: !givenUp -> m2A!0, id, dummy; givenUp = true; gUp[id] = true;
            fi;
        }
        stateB = submittedB;
    ::(stateB == submittedB) -> printf("Bid submitted\n");
        printf("Waiting for the result now\n");
        if
        ::m2B[id]?0, status ->
            printf("Bid too low\n");
            stateB = idleB;
        ::m2B[id]?0, winner->
            printf("Hurray, I won\n");
            stateB = idleB;
        ::m2B[id]?0, loser ->
            printf("I lost :(\n");
            stateB = idleB;
        fi;
    od;
}


/*Auction process*/

proctype auctioneer() {
    int round = 0;
    int i = 0;
    int idcount = 0;
    stateA = waitA;
    int bid;
    int id;
    int max_bid;
    int max_id;
    do
    :: true -> if
        :: (stateA == waitA) -> printf("Waiting to start the auction\n");
            m2A?0, 0, start_auction;
            printf("Ready to get the auction started\n");
            do
            :: (i<amountOfClients) -> m2B[i]!0,auction_started;
                i = i+1;
            :: (i==amountOfClients) -> i = 0;
                break;
            od;
            stateA = startA;
            printf("Sending start signal\n");
        :: (stateA == startA) -> printf("Waiting for a bid to be submitted....\n");
            if
            :: !gUp[idcount] || max_id==idcount -> /*continue*/;
            fi;
            m2B[idcount]!0,send_bid;
            printf("Waiting for a bid to be submitted by %d....\n",idcount);
            m2A?bid, id, dummy;
            printf("Client bid received\n");
            idcount = idcount + 1;
            if
            :: (idcount==amountOfClients) -> idcount = 0; givenUp = false;
            :: else -> skip;
            fi;
            stateA=processBidA;
        :: (stateA == processBidA) -> printf("Computing if it is winning bid\n");
            if
            :: bid>max_bid && bid>=startBid -> m2B[id]!0, status;stateA=startA; max_bid = bid; max_id=id;
            :: bid<startBid -> m2B[id]!0, status;stateA=startA;
                    
            fi;
        :: (stateA == endA) -> printf("Winner elected.Auction will terminate\n");
            do
            :: (i<amountOfClients) -> m2B[i]!0,end_auction;
                i = i+1;
            :: (i==amountOfClients) -> i = 0;
                break;
            od;
            break;
        fi;
    round = round + 1;
    od;
}
